Math 512: Finite Model Theory Fixed Point logics

John Baldwin

February 16, 1997

References: E and F: 6., 7; Vaananen chapter 3.

Moschovakis, \underline{Elementary Induction on Abstract Structures}, North Holland; Barwise and Feferman \underline{Model Theoretic Logics}, Springer, 1985.

0.1 Definition. Let K be a class of L-structures. An n-ary global relation on K is a function Γ such that for each A, Γ(A) is an n-ary relation on A, which is preserved by isomorphism.

Examples: any logical formula; if R is a binary relations symbol, the transitive closure of R, connectivity is a 0-ary global relation on graphs.

Let F be a function from P(X) to P(X). F is called inflationary if X ⊆ F (X). F is called monotone if X ⊆ Y implies F (X) ⊆ F (Y). F^{0}(X) = ∅, F^{i+1}(X) = F (F^{i}(X)). For any F, F̂(X) = X ∪ F (X) is inflationary.

If F is inflationary or monotone (since we begin with ∅), F^{i}(X) ⊆ F^{i+1}(X). Thus, if X is finite, there is an i such that F_{∞} = F^{i+1}(X) = F^{i}(X). F^{i}(X) is the least fixed point of F.

There are several choices for exactly how to form a logic incorporating inductive definitions. We deal first with inflationary and the positive inductive definitions.

For any formula ϕ(\overline{x}, S), the operator F^{ϕ(\overline{x},S)∨S\overline{x}}(A) = \{\overline{a} : A ⊧ ϕ(\overline{a}, S) ∨ S\overline{a} is inflationary. The least fixed point F_{∞}^{ϕ(\overline{x},S)∨S\overline{x}} is called the inflationary fixed point of ϕ.

0.2 Definition. F_{∞}^{ϕ(S)} is a global relation. We define a new formula by [IF P_{\overline{x},X}ϕ]\overline{t} = ψ(\overline{t}) with semantics A ⊧ ψ(\overline{a}) iff \overline{a} ∈ F_{∞}^{X\overline{x}∨ϕ}. We form Inflationary Fixed Point logic IFP by closing under first order operations.

A symbol S occurs positively in a formula ϕ if it is in the scope of an even number of negation symbols (Boolean connectives are ∧, ∨, ¬.). If S occurs positively in ϕ, the operator F^{ϕ(S)}(A) = \{\overline{a} : A ⊧ ϕ(\overline{a}, S) is monotone. F_{∞}^{ϕ(S)} is the least fixed point of this operator.

E.g. transitive closure, subgroup generated by (an operator can have more than one fixed point), ‘even’ or ‘odd’ elements of a successor chain.

To have a decidable syntax, we add this quantifier only when S occurs positively in ϕ. Gurevich showed it is undecidable to just ask for F^{ϕ(S)} monotone.

0.3 Definition. Least Fixed Point Logic LPF contains exactly those sentences of IFP in which all instances of the fixed point operator on (\overline{x}, X) have X occuring positively. Thus, F^{ϕ(X)} is monotone, so we define a new formula by [LF P_{\overline{x},X}ϕ]\overline{t} = ψ(\overline{t}) with semantics A ⊧ ψ(\overline{a}) iff \overline{a} ∈ F_{∞}^{X\overline{x}}.

We don’t need ∨X\overline{x} in the superscript because X occurs positively.

0.4 Theorem. (Gurevich and Shelah) LF P -logic = IF P logic.

After proving the result we will follow Vaananen and write F P for this logic. But for the proof we need a number of new ideas and lemmas.

0.5 Digression. Comparing logics. What does equality mean in this lemma? For that matter, what is a logic?

0.6 Definition. A logic is a pair L, ⊧_{L} such that for each vocabulary (similarity type, language) τ, L(τ) is a collection of sentences ϕ such that for τ-structure A either A ⊧_{L} ϕ or not. This pair should satisfy certain regularity conditions with we don’t enumerate here. See E and B article in Barwise et al.

0.7 Definition. L_{∞} ≤ L_{∈} if for every vocabulary τ and every L_{∞}(τ)-sentence ϕ, there is an L_{∞}(τ)-sentence ψ such that for all A, A ⊧_{L_{∞}} ϕ iff A ⊧_{L_{∈}} ψ. Equivalence of logics is derived in the obvious way.

0.8 Example: Simultaneous Induction. Let A, E be a graph. Let

ϕ_{1}(x, y, S, T) = Exy ∨ (∃z)(Sxz ∧ Ezy); ϕ_{2}(x, y, S, T) = (∃z)(∃w)(T xz ∧ T xw ∧ Ezw).

The fixed point of the first formula is the transitive closure of E; of the second is the collection of all elements that are in cycles. (Assignment: explain 7.1.16 of E and F and last paragraph on page 186.)

0.9 Definition. (Simultaneous Fixed Points)

1. if S_{0} = T_{0} = ∅, S_{i+1} = \{\overline{a} : ϕ(\overline{a}, S^{i}, T^{i}), T_{i+1} = \{\overline{b} : ϕ(\overline{a}, S^{i}, T^{i}), there is a j with S_{j+1} = S_{j} and T_{j+1} = T_{j}, (S_{j}, T_{j}) is the simultaneous fixed point.

2. A (rather awkward) syntax for a simultaneous fixed point logic is described at E and F pg. 173.

Remark. If S_{∞} and T_{∞} are fixed points of ϕ(\overline{x}, S), ψ(\overline{x}, T) then S_{∞} ∩ T_{∞} is a simultaneous fixed point of the system [LF P_{\overline{x}S}ϕ(\overline{x}, S)], [LF P_{\overline{x}T} ϕ(\overline{x}, T)], [LF P_{\overline{x}R}S(\overline{x} ∧ T (\overline{x})]. (Note that R does not occur in the third formula.) This is a step toward showing that every formula in FP is equivalent to one involving only one application of the fixed point operator.

As shorthand Vaananen writes ψ(\overline{x}, S, R, T) ↔ [LF P_{\overline{x}R}S(\overline{x} ∧ T (\overline{x})].

0.10 Lemma. Let ϕ_{1}(\overline{x}, S, T) and ϕ_{2}(\overline{y}, S, T) both be positive in the k-ary predicates S and T. Then there is a formula θ(t, \overline{x}, \overline{y}, U), positive in the 2k + 1-ary predicate U, such that the simultaneous fixed points of S and T are sections of the fixed point of U.

Proof. Fix c_{0}, c_{1}, \overline{a}, \overline{b} (of length k) in A. (\overline{a}, \overline{b} could be sequences of c_{i}). Let θ(t, \overline{x}, \overline{y}, U) be

[t = c_{0}∧ϕ_{1}(\overline{x}, \{\overline{y}′ : U(c_{0}, \overline{y}′, \overline{a})\}, \{\overline{x}′ : U(c_{1}, \overline{b}, \overline{x})\}]∨[t = c_{1}∧ϕ_{2}(\overline{y}, \{\overline{y}′ : U(c_{0}, \overline{y}′, \overline{a}\}, \{\overline{x}′ : U(c_{1}, \overline{b}, \overline{x})\}].

Now,

[LF P_{\overline{x},S}ϕ_{1}]⟨v_{1}, … v_{k}⟩ = [LF P_{w_{o}\overline{x}\overline{y},U}θ]c_{0}\overline{v}\overline{a}
[LF P_{\overline{y},T} ϕ_{2}]⟨v_{k+1}, … v_{2k}⟩ = [LF P_{w_{o}\overline{x}\overline{y},U}θ]c_{1}\overline{b}⟨v_{k+1}, … v_{2k}⟩.

0.11 Definition. Suppose ϕ(\overline{x}, S) is positive in S. On a structure A we define:

1. |ϕ| = least i such that S^{i+1} = S^{i}.

2.

|a| = \{ \begin{matrix}least i such that \overline{a} ∈ S^{i}, & if \overline{a} ∈ S^{∞} \\ |ϕ| + 1 & otherwise \end{matrix}

The result is due to Moschovakis; this proof is by Leivant. In fact, the argument is part of the more general argument of Gurevich-Shelah for IFP=LFP.

Lemma 0.12 (Stage Comparison Theorem). Suppose ϕ(\overline{x}, S) is positive in S. The global relations:

\overline{x} ≺_{ϕ} \overline{y} ↔ |\overline{x}| < |\overline{y}|
\overline{x} ≤_{ϕ} \overline{y} ↔ |\overline{x}| ≤ |\overline{y}| ∧ \overline{x} ∈ S^{∞}

and their complements ⊀_{ϕ} and ≰_{ϕ} are in FP.

Proof. Define also

\overline{x} ≺_{1}^{ϕ} \overline{y} ↔ |\overline{x}| + 1 = |\overline{y}|

To save clutter we drop the bars from \overline{x}, \overline{y}; we write · ≺ y for \{u : u ≺ y\}. We simultaneously induct on the following 5 formulas (see pg 25 of Vaananen for interpretation):

1. [LF P_{xy,≺}(∃z)(x ≤ z ≺_{1} y)]

2. [LF P_{xy,≤}ϕ(x, · ≺ y)]

3. [LF P_{xy,≺_{1}} {ϕ(x, · ≺ x) ∧ ¬ϕ(y, ¬· ⊀ x) ∧ [(ϕ(y, · ≤ x) ∨ (∀z)(ϕ(z, ¬· ≰ x) → ϕ(z, · ≺ x))]}]

4. [LF P_{xy,⊀}(∃z)(x ≰ z ≺_{1} y ∨ ϕ(y, ∅) ∨ (∀z)ϕ(z, ∅)]

5. [LF P_{xy,≰}¬ϕ(x, ¬· ⊀ y)]

We need to make two observations: the above formulas are positive in the new predicates so a fixed point exists; the simultaneous fixed point (≺, ≤, ≺_{1}, ⊀, ≰) of this induction is (≺_{ϕ}, ≤_{ϕ}, ≺_{1}^{ϕ}, ⊀_{ϕ}, ≰_{ϕ}).

0.13 Proof of Theorem 0.4. Clearly LF P ≤ IF P. For the converse, it suffices to show inductively that for any LF P -formula ϕ(\overline{x}, X) (where X may occur negatively, [IF P_{\overline{x},X}ϕ]\overline{t} is equivalent to a formula in LF P.

First rewrite ϕ(\overline{x}, X) as ψ(\overline{x}, Y, X) which is positive in both X and Y, by replacing each occurence of X with ¬Y. So ϕ(x, X) ↔ ψ(\overline{x}, X^{c}, X) defines the inductive step. Note that we can define ≤_{ϕ} just as for a monotone formula. Moreover:

⊧_{fin} [IF P_{\overline{x},X}ϕ] ↔ \overline{x} ≤_{ϕ} \overline{x}

and

{u : u ≤_{ϕ} x}^{c} = {u : x ≺_{ϕ} u}.

So it suffices to show (by a variant of the stage comparison theorem) that ≤^{ϕ} is definable as a LFP. We simultaneously induct on the following 2 formulas.

[LF P_{xy,≤}(ϕ(x, ∅) ∧ ϕ(y, ∅)) ∨ (∃z)z ≺ y ∧ ψ(x, · ≤ z, z ≺ ·) ∧ ψ(y, · ≤ z, z ≺ ·)]

[LF P_{xy,≺}((ϕ(x, ∅) ∧ ¬(ϕ(y, ∅)) ∨ (∃z)(z ≤ z ∧ ψ(x, · ≤ z, z ≺ ·) ∧ ¬ψ(y, ¬z ≺ ·, ¬· ≤ z)].

These formulas are positive in ≤, ≺ so there is a fixed point. Let ≤_{ϕ}^{n}, ≺_{ϕ}^{n} denote the nth iterate towards this fixed point. We prove by simultaneous induction on n:

a ≤_{b}^{n} iff a, b ∈ F_{ϕ}^{n} and a ≤_{ϕ}^{n} b
a ≺_{b}^{n} iff a, b ∈ F_{ϕ}^{n} and a ≺_{ϕ}^{n} b

Here is the induction step for the first equivalence:

a ≤^{n+1} b iff

(ϕ(a, ∅) ∧ ϕ(b, ∅)) ∨ (∃z)(z ≺^{n} b ∧ ψ(a, · ≤^{n} z, z ≺^{n} ·) ∧ ψ(b, · ≤^{n} z, z ≺^{n} ·)).

By induction this is equivalent to

(ϕ(a, ∅) ∧ ϕ(b, ∅)) ∨ (∃z)(z ∈ F_{ϕ}^{n} ∧ ψ(a, · ≤_{ϕ}^{n} z, z ≺_{ϕ}^{n} ·) ∧ ψ(b, · ≤_{ϕ}^{n} z, z ≺_{ϕ}^{n} ·)).

By the choice of ϕ, ψ this is equivalent to:

(ϕ(a, ∅) ∧ ϕ(b, ∅)) ∨ (∃z)(z ≺_{ϕ}^{n} y ∧ a, b ∈ F^{ϕ}(F_{n}^{ϕ})).

Which is then equivalent to: a ≤_{ϕ}^{n} b ∧ a, b ∈ F_{n+1}^{ϕ}.

This shows that the stage comparison relations of H can be given by a positive inductive definition (i.e. are in LPF).

0.14 Corollary. (Immerman) Every formula of LFP can be given by a single positive induction.

Proof. (idea) We checked ’and’ earlier. For the existential quantifier and iterating LPF see 7.2.4 of E and F. This is the transitivity lemma. We need to show that ¬[LF P_{\overline{x},S}ϕ]\overline{t}. The key is that ¬[LF P_{\overline{x},S}ϕ]\overline{t} is equivalent to

(∀\overline{x})¬ϕ(\overline{x}, ∅) ∨ ((∃\overline{x})ϕ(\overline{x}, ∅) ∧ ((∃\overline{z})ϕ_{|ϕ|}(\overline{z}) ∧ \overline{z} ≺_{ϕ} \overline{t}))

where ϕ_{|ϕ|}(\overline{z}) means (∀\overline{v})(\overline{v} ≤_{ϕ} \overline{z} ∨ (¬ψ(\overline{v}, ¬\overline{z} ≺ ·, ¬· ≤ \overline{z})). (No element comes in at the stage after \overline{z}.) Note that the number |ϕ| is depends on the structure A.

Coming attraction:

0.15 Lemma. F O ⊆ F P ⊆ P T IME.